Termination w.r.t. Q proof of /tmp/tmpQjEgSN/mapHard.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

AP(ap(ap(if, false), f), xs) → AP(f, ap(last, xs))
AP(ap(ap(if, false), f), xs) → AP(cons, ap(f, ap(last, xs)))
AP(ap(ap(if, false), f), xs) → AP(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
AP(ap(ap(if, false), f), xs) → AP(map, f)
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(ap(if, false), f), xs) → AP(dropLast, xs)
AP(ap(ap(if, false), f), xs) → AP(last, xs)
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
AP(ap(ap(if, false), f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(ap(map, f), xs) → AP(ap(if, ap(isEmpty, xs)), f)
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
AP(ap(map, f), xs) → AP(if, ap(isEmpty, xs))
AP(ap(map, f), xs) → AP(isEmpty, xs)

The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

AP(ap(ap(if, false), f), xs) → AP(f, ap(last, xs))
AP(ap(ap(if, false), f), xs) → AP(cons, ap(f, ap(last, xs)))
AP(ap(ap(if, false), f), xs) → AP(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
AP(ap(ap(if, false), f), xs) → AP(map, f)
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(ap(if, false), f), xs) → AP(dropLast, xs)
AP(ap(ap(if, false), f), xs) → AP(last, xs)
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
AP(ap(ap(if, false), f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(ap(map, f), xs) → AP(ap(if, ap(isEmpty, xs)), f)
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
AP(ap(map, f), xs) → AP(if, ap(isEmpty, xs))
AP(ap(map, f), xs) → AP(isEmpty, xs)

The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 9 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))

The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(ap(x₁, x₂)) = (2)x_1 + (4)x_2
POL(cons) = 4
POL(AP(x₁, x₂)) = (4)x_2
POL(dropLast) = 0

The value of delta used in the strict ordering is 256.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))

The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(ap(x₁, x₂)) = (4)x_1 + (9/4)x_2
POL(cons) = 2
POL(AP(x₁, x₂)) = (3/2)x_2
POL(last) = 0

The value of delta used in the strict ordering is 108.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

AP(ap(ap(if, false), f), xs) → AP(f, ap(last, xs))
AP(ap(ap(if, false), f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)

The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

AP(ap(ap(if, false), f), xs) → AP(f, ap(last, xs))

The remaining pairs can at least be oriented weakly.

AP(ap(ap(if, false), f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)

Used ordering: Polynomial interpretation [25,35]:

POL(ap(x₁, x₂)) = 13/4 + (2)x_2
POL(cons) = 7/4
POL(AP(x₁, x₂)) = (2)x_1
POL(if) = 0
POL(last) = 15/4
POL(map) = 0
POL(true) = 3/2
POL(false) = 2
POL(isEmpty) = 4
POL(dropLast) = 5/2
POL(nil) = 1/4

The value of delta used in the strict ordering is 13/2.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

AP(ap(ap(if, false), f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)

The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.